COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00011 ENDMK
C⊗;

(DE ANA (F ;; X VARS BODY DECVARS)
  (SETQ X (GET F 'EXPR)
        VARS (CADR X)
        BODY (CADDR X))
  (LET ((E BODY)) (COND
    ((ATOM E))
    ((MEMQ (CAR E) '(CAR CDR SUB1))
     (IF (ATOM (CADR E))
         (AND (MEMQ (CADR E) VARS)
              (OR (MEMQ (CADR E) DECVARS)
                  (SETQ DECVARS (CONS (CADR E) DECVARS))))
         (SELF (CADR E))))
    (T (SELF (NEXTL E)) (SELF E))))
  (PUT F VARS 'VARS)
  (PUT F BODY 'BODY)
  (PUT F DECVARS 'DECVARS)
  )

(DE VARS (F) (GET F 'VARS))
(DE BODY (F) (GET F 'BODY))
(DE DECVARS (F) (GET F 'DECVARS))


; ****** EVALUATEUR SYMBOLIQUE ******* ;

(DE RED (E AL) (COND
  ((ATOM E) (LET ((VAL (ASSQ E AL)))
                 (IF VAL (CADR VAL) E)))
  ((EQ (CAR E) 'IF)
   (LET ((TEST (RED (CADR E) AL))) (COND
      ((NULL TEST) (RED (CADDDR E) AL))
      ((OR (EQ TEST T) (EQ (CAR TEST) 'CONS))
       (RED (CADDR E) AL))
      (T (CONS 'IF (CONS TEST (CDDR E)))))))
   (T (LET ((LARGS (MAPCAR (CDR E) '(LAMBDA (E) (RED E AL))))
            (FUN (CAR E)))
        (SELECTQ FUN
          (CAR (IF (EQ (CAAR LARGS) 'CONS)
                   (CADAR LARGS)
                   (CONS FUN LARGS)))
          (CDR (IF (EQ (CAAR LARGS) 'CONS)
                   (CADDR (CAR LARGS))
                   (CONS FUN LARGS)))
          (SUB1 (IF (EQ (CAAR LARGS) 'ADD1)
                    (CADAR LARGS)
                    (CONS FUN LARGS)))
          (ADD1 (CONS FUN LARGS))
          (CONS (CONS FUN LARGS))
          (ZEROP (COND ((ZEROP (CAR LARGS)) T)
                       ((EQ (CAAR LARGS) 'ADD1) NIL)
                       (T (CONS FUN LARGS))))
          (NULL  (COND ((NULL (CAR LARGS)) T)
                       ((EQ (CAR LARGS) T) NIL)
                       ((EQ (CAAR LARGS) 'CONS) NIL)
                       (T (CONS FUN LARGS))))
          (T (LET ((AL1 (REDPAIR FUN (VARS FUN) LARGS)))
                  (IF (EQ AL1 'NO) (CONS FUN LARGS)
                      (RED (BODY FUN) (NCONC AL1 AL)))))
  )))
  ))

; ****** CONTROLEUR DE DEPLOIEMENT ****** ;

(DE REDPAIR (FUN VARS LARGS ;; DECVARS RES V L)
  (ESCAPE EXIT
    (SETQ DECVARS (DECVARS FUN))
    (WHILE VARS
      (SETQ V (NEXTL VARS) L (NEXTL LARGS))
      (IF (MEMQ V DECVARS)
          (AND (NEQ L NIL) (NEQ L 0)
               (NEQ (CAR L) 'CONS) (NEQ (CAR L) 'ADD1)
               (EXIT 'NO)))
       (SETQ RES (CONS (LIST V L) RES)))
     RES))





; ******** QUELQUES FONCTIONS DE TEST ********* ; 

(DE LOOP () (PRINT 'EVAL 'SYM ) (PRINT (RED (READ) ())) (TERPRI) (LOOP))

(PROGN

(DE APP (X Y) (IF (NULL X) Y (CONS (CAR X) (APP (CDR X) Y))))
(ANA 'APP)

(DE REV (X) (IF (NULL X) NIL (APP (REV (CDR X)) (CONS (CAR X) NIL))))
(ANA 'REV)

(DE LEN (L) (IF (NULL L) 0 (ADD1 (LEN (CDR L)))))
(ANA 'LEN)

(DE P (X Y) (IF (ZEROP X) Y (ADD1 (P (SUB1 X) Y))))
(ANA 'P)

(DE M (X Y) (IF (ZEROP X) 0 (P Y (M (SUB1 X) Y))))
(ANA 'M)
)

; ******** LE-PROOF-VERIFIEUR ******** ;

(DF THEO (L)
  (PROVE L 0))


; EX: (THEO (P M N) = (P N M)) ;

(DE PROVE (TH N ;; THH)  ; TH = ( * = ** ) ;
  (PSTAR (NCONC (LIST N 'PROVE) TH))
  (COND
    ((EQ (SETQ THH (REDUCE TH)) T))
    ((EQUAL TH THH) (COMMAND))
    (T (PROVE THH (ADD1 N))))
  (PSTAR (LIST N 'PROVED)))

(DE PSTAR (L)
  (PRIN1 '********)
  (APPLY 'PRINT L))


(DE COMMAND (;; COM PAT REMP NBOC)
  (PRINT 'COMMAND '/?)
  (SETQ COM (READ))
  (SELECTQ (CAR COM)
    (INDUCT (COND ((EQ (CADR COM) 'LIST)
                   (LISTINDUCT (CADDR COM) TH))
                  ((EQ (CADR COM) 'NUM)
                   (NUMINDUCT (CADDR COM) TH))
                  (T (PRINT 'WRONG 'TYPE)
                     (COMMAND))))
    (INDHYP (SETQ NBOC (CADR COM))
            (IF (EQ (CADDR COM) '->)
                (SETQ PAT (CAR IH) REMP (CADDR IH))
                (SETQ PAT (CADDR IH) REMP (CAR IH)))
            (PROVE (USEINDHYP TH) (ADD1 N)))
    (GEN (PROVE (LET ((TH TH) (LSUB (CDR COM)))
                  (IF LSUB 
                      (SELF (SUBSTEQUAL (NEXTL LSUB) (NEXTL LSUB) TH)
                            LSUB)
                      TH))
                (ADD1 N)))
    (LOOK (PRINT (EVAL (CADR COM))) (COMMAND))
    (T (PRINT 'UNKNOWN 'COMMAND) (COMMAND))
  ))

(DE REDUCE (THH ;; X Y)
  (SETQ X (RED (CAR THH) NIL)
        Y (RED (CADDR THH) NIL))
  (OR (EQUAL X Y)
      (LIST X '= Y))
  )



(DE LISTINDUCT (VAR IH) ; IH = INDUCTION HYPOTHESIS ;
  (PSTAR (LIST 'BASE))
  (PROVE (SUBST NIL VAR IH) (ADD1 N))
  (PSTAR (LIST 'STEP))
  (PROVE (SUBST (LIST 'CONS (GENSYM VAR '/:) VAR) VAR IH) (ADD1 N))
  )

(DE NUMINDUCT (VAR IH)
  (PSTAR (LIST 'BASE))
  (PROVE (SUBST 0 VAR IH) (ADD1 N))
  (PSTAR (LIST 'STEP))
  (PROVE (SUBST (LIST 'ADD1 VAR) VAR IH) (ADD1 N))
  )


(DE USEINDHYP (TH) (COND
  ((ATOM TH) (IF (NEQ TH PAT) TH
                 (SETQ NBOC (SUB1 NBOC))
                 (IF (ZEROP NBOC) REMP TH)))
  ((EQUAL TH PAT) (SETQ NBOC (SUB1 NBOC))
                  (IF (ZEROP NBOC) REMP
                      (CONS (USEINDHYP (NEXTL TH))
                            (USEINDHYP TH))))
  (T (CONS (USEINDHYP (NEXTL TH))
           (USEINDHYP TH)))
  ))


(DE SUBSTEQUAL (X Y TH) (COND
  ((EQUAL Y TH) X)
  ((ATOM TH) TH)
  (T (CONS (SUBSTEQUAL X Y (NEXTL TH))
           (SUBSTEQUAL X Y TH)))))